a, b:Id. a = b  a = b 

latex

Definitions	t  T, Id, Prop, P  Q, P  Q, P & Q, P  Q, IdDeq, x:A. B(x), eqof(d), b, a = b
Lemmas	iff functionality wrt iff, deq property, assert wf, eqof wf, id-deq wf, Id wf